A:Type, I:MaInterface(A), i:Id.
(i  ma-interface-locs(I))
 (k:Knd.
 (k  ma-interface-dom(I;i))
  (ma-interface-msgs(I;i;k)
  ( State(ma-interface-ds(I;i))ma-interface-valtype(I;i;k)(A List))) 

latex

Definitions

Type, b, a:A fp B(a), MaInterface(T), Atom$n, Id, s = t, a < b, (x  l), left + right, Knd, t  T, {x:A| B(x)} , x:AB(x), x:A. B(x), Top, x. t(x), State(ds), x:A  B(x), type List, <a, b>, let x,y = A in B(x;y), f(a), P  Q, , A, P & Q, P  Q, Unit, t.1, ma-interface-valtype(I;i;k), x.A(x), ma-interface-ds(I;i), ma-interface-code(I;i;k), do-apply(f;x), [car / cdr], if b then t else f fi , S  T, can-apply(f;x), f(x)?z, ma-interface-msgs(I;i;k)

Lemmas

ma-interface-valtype wf, can-apply wf, ifthenelse wf, do-apply wf, ma-interface-code wf, decl-state wf, ma-interface-ds wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-trivial-subtype-top